Issue2522.agda:17,44-45
x₁ != ∞ of type Size
when checking that the expression y has type D (λ _ → A ∞) ∞
